$\forall$${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} , $P$, $Q$:(\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} . $P$($e$) $\Leftarrow\!\Rightarrow$ $Q$($e$)) $\Rightarrow$ ($\forall$$e$$\in$[$e_{1}$,$e_{2}$).$P$($e$) $\Leftarrow\!\Rightarrow$ $\forall$$e$$\in$[$e_{1}$,$e_{2}$).$Q$($e$))